Nuprl Definition : R-icompat
0,22
postcript
pdf
R-icompat(
A
;
B
)
== if Rplus?(
A
)
R-icompat(Rplus-left(
A
);
B
) & R-icompat(Rplus-right(
A
);
B
)
== i
; Rplus?(
B
)
R-icompat(
A
;Rplus-left(
B
)) & R-icompat(
A
;Rplus-right(
B
))
== i
; Rnone?(
A
)
True
== i
; Rnone?(
B
)
True
== i
; R-loc(
A
) = R-loc(
B
)
True
==
else R-interface-compat(
A
;
B
) & R-interface-compat(
B
;
A
) fi
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
Rplus?(
x1
)
,
Rplus-left(
x1
)
,
f
(
a
)
,
Rplus-right(
x1
)
,
Rnone?(
x1
)
,
if
b
t
else
f
fi
,
a
=
b
,
R-loc(
R
)
,
True
,
P
&
Q
,
R-interface-compat(
A
;
B
)
FDL editor aliases
R-icompat
origin